/* test if while statement */
/*@ */
int max(array[10,int] a)
{
	int i;
	int m;
	i=0;
	m = a[0];
	while(i<10)/*@ forall j:int.((j>=0)&&(j<i)&&(a[j]<=m)) */
	{
		if(a[i]>m) //No else
			m=a[i];
		i=i+1;
	}
	return m;
}
/*@ forall j:int.((j>=0)&&(j<10)&&(a[j]<=result))*/

/*@*/
array[10,int] init()
{
  int i;
  array[10, int] a;
  i=0;
  while(i<10)/*@i>=0&&i<10*/
  {
    a[i] = i * i;
    i=i+1;
  }
  return a;
}
/*@*/

/*@ */
void main()
{
  array[10,int] a;
  int m;
  a=init();
  m=max(a);
  print(m);
  return;
}
/*@ */
